Nuprl Lemma : es-trans_wf
11,40
postcript
pdf
es
:event_system{i:l},
i
:Id.
es-trans(
es
;
i
)
k
:Knd
es-kindtype(
es
;
i
;
k
)
es_state(
es
;
i
)
es_state(
es
;
i
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
es-V(
es
)
,
f
(
a
)
,
x
:
A
B
(
x
)
,
subtype(
S
;
T
)
,
es-M(
es
)
,
tag(
k
)
,
lnk(
k
)
,
act(
k
)
,
islocal(
k
)
,
isrcv(
k
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
))
,
es-kindtype(
es
;
i
;
k
)
,
x
:
A
B
(
x
)
,
left
+
right
,
Knd
,
event_system{i:l}
,
Id
,
Type
,
es_state(
es
;
i
)
,
IdLnk
,
x
,
y
.
t
(
x
;
y
)
,
x
.
t
(
x
)
,
es-Trans(
es
)
,
suptype(
S
;
T
)
,
es-trans(
es
;
i
)
Lemmas
es-Trans
wf
,
Knd
wf
,
kindcase
wf
,
IdLnk
wf
,
es
state
wf
,
es-kindtype
wf
,
Id
wf
,
event
system
wf
,
es-M
wf
,
es-V
wf
origin
es:event_system{i:l}, i:Id.
k:Knd
es-kindtype(es; i; k)es_state(es; i)es_state(es; i) es:event_system{i:l}, i:Id.
k:Kndes-kindtype(es; i; k)es_state(es; i)es_state(es; i) 
B(x)
x,y. t(x;y)